Nuprl Lemma : rel_plus_strongwellfounded 0,22

T:Type, R:(TTProp). SWellFounded(x R y SWellFounded(x R^+ y
latex


DefinitionsUnit, P  Q, , b, b, i=j, P & Q, SWellFounded(R(x;y)), R^+, x:AB(x), , x f y, rel_exp(T;R;n), , A, False, AB, Dec(P), P  Q, Prop, t  T, SQType(T), x:AB(x), P  Q, {T}
Lemmasdecidable int equal, le wf, rel exp wf, nat wf, nat plus properties, nat plus wf, rel plus wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert

origin